// Google test includes
#include <gtest/gtest.h>
#include <gmock/gmock.h>

#include <memory>

// Tested file
#include "Processors/NNF/Classic.h"

// Helper classes
#include "Nodes/Binary/Node.h"
#include "Parsers/PostfixParser.h"
#include "Printers/PostfixPrinter.h"
#include "Printers/PrettyPrinter.h"
#include "Printers/Printer.h"

using namespace testing;

TEST(ClassicNNFProcessorTest, NotAnd)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory);

	// Check processing of ~(A & B) -> ~A | ~B
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB&~", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("A~B~|", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, NotOr)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory);

	// Check processing of ~(A | B) -> ~A & ~B
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB|~", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("A~B~&", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, NotNot)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory);

	// Check processing of ~~A -> A
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("A~~", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("A", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, OrAnd1)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory);

	// Check processing of (A & B) | C -> (A & C) | (B & C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB&C|", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AC&BC&|", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, OrAnd2)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory);

	// Check processing of A | (B & C) -> (A & B) | (A & C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("ABC&|", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AB&AC&|", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, OrAndNotAppliedInCNFMode)
{
	// Prepare factory and processor in CNF mode
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory, CNF);

	// Both following statements shall not be changed in CNF mode
	std::auto_ptr<BinaryNode> node1(postfixParse<BinaryNode>("AB&C|", factory));
	EXPECT_FALSE(processor(node1));
	std::auto_ptr<BinaryNode> node2(postfixParse<BinaryNode>("ABC&|", factory));
	EXPECT_FALSE(processor(node2));
}

TEST(ClassicNNFProcessorTest, AndOr1)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory, CNF);

	// Check processing of (A | B) & C -> (A | C) & (B | C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("AB|C&", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AC|BC|&", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, AndOr2)
{
	// Prepare factory and processor
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory, CNF);

	// Check processing of A & (B | C) -> (A | B) & (A | C)
	std::auto_ptr<BinaryNode> node(postfixParse<BinaryNode>("ABC|&", factory));
	EXPECT_TRUE(processor(node));
	EXPECT_EQ("AB|AC|&", PostfixPrinter<BinaryNode>::print(node.get()));
}

TEST(ClassicNNFProcessorTest, AndOrNotAppliedInDNFMode)
{
	// Prepare factory and processor in CNF mode
	NodeFactory<BinaryNode> factory;
	NNFProcessor<BinaryNode, NodeFactory<BinaryNode> > processor(factory, DNF);

	// Both following statements shall not be changed in DNF mode
	std::auto_ptr<BinaryNode> node1(postfixParse<BinaryNode>("AB|C&", factory));
	EXPECT_FALSE(processor(node1));
	std::auto_ptr<BinaryNode> node2(postfixParse<BinaryNode>("ABC|&", factory));
	EXPECT_FALSE(processor(node2));
}


